Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
top(sent(x)) |
→ top(check(rest(x))) |
| 2: |
|
rest(nil) |
→ sent(nil) |
| 3: |
|
rest(cons(x,y)) |
→ sent(y) |
| 4: |
|
check(sent(x)) |
→ sent(check(x)) |
| 5: |
|
check(rest(x)) |
→ rest(check(x)) |
| 6: |
|
check(cons(x,y)) |
→ cons(check(x),y) |
| 7: |
|
check(cons(x,y)) |
→ cons(x,check(y)) |
| 8: |
|
check(cons(x,y)) |
→ cons(x,y) |
|
There are 8 dependency pairs:
|
| 9: |
|
TOP(sent(x)) |
→ TOP(check(rest(x))) |
| 10: |
|
TOP(sent(x)) |
→ CHECK(rest(x)) |
| 11: |
|
TOP(sent(x)) |
→ REST(x) |
| 12: |
|
CHECK(sent(x)) |
→ CHECK(x) |
| 13: |
|
CHECK(rest(x)) |
→ REST(check(x)) |
| 14: |
|
CHECK(rest(x)) |
→ CHECK(x) |
| 15: |
|
CHECK(cons(x,y)) |
→ CHECK(x) |
| 16: |
|
CHECK(cons(x,y)) |
→ CHECK(y) |
|
The approximated dependency graph contains 2 SCCs:
{12,14-16}
and {9}.
-
Consider the SCC {12,14-16}.
There are no usable rules.
By taking the AF π with
π(CHECK) = π(rest) = π(sent) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {12,14}
are weakly decreasing and
the rules in {15,16}
are strictly decreasing.
There is one new SCC.
-
Consider the SCC {12,14}.
By taking the AF π with
π(CHECK) = π(rest) = 1 together with
the lexicographic path order with
empty precedence,
rule 14
is weakly decreasing and
rule 12
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {14}.
By taking the AF π with
π(CHECK) = 1 together with
the lexicographic path order with
empty precedence,
rule 14
is strictly decreasing.
-
Consider the SCC {9}.
The usable rules are {2-8}.
The constraints could not be solved.
Tyrolean Termination Tool (0.05 seconds)
--- May 4, 2006